Inference at * 1 2 1 
Iof proof for Lemma append overlapping sublists:

.....wf..... NILNIL

1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||  0 
  (i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi )
   {0..||L1 @ [x / L2]||}{0..||L||} 

latex

 by InteriorProof ((((((MemCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
CollapseTHENA ((Au),(first_nat 3:n)) (first_tok :t) inil_term)))) 
CollapseTHEN (SplitOnConclITE
CollapseTHEN (Spli))) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
CollapseTHEN ((Aut)) (first_tok SupInf:t) inil_term))) 

latex

C.

Definitions	T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , x:A. B(x), True, False, Y, t  ...$L, A  B, , t  T, i  j , A, ||as||, P  Q, Unit, , {i..j},
Lemmas	int seg wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, length nil, length append, append wf, non neg length, length cons, le wf, assert wf, bool wf, length wf1, le int wf